Example 6 in [Lucas - JFLP'98]

Summary: Ex6_Luc98

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Zantema's transformation (Polynomials @ MuTerm)
  3. Ferreira and Ribeiro's transformation (DPs @ CiME)
  4. Giesl and Middeldorp's transformation (DPs @ CiME)
  5. CSRPO
  6. Polynomial interpretation (MuTerm)
  7. CSDP

CS-TRS Ex6_Luc98 (file Ex6_Luc98.csr)

Functions:  first 0 nil s cons from

Constructors:  0 nil s cons

Variables:  X Y Z

Arities: 

ar(first) = 2
ar(0) = 0
ar(nil) = 0
ar(s) = 1
ar(cons) = 2
ar(from) = 1

Replacement map: 

µ(first)={1,2}
µ(0)={}
µ(nil)={}
µ(s)={1}
µ(cons)={1}
µ(from)={1}

Rules:  (file Ex6_Luc98) 

first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
from(X) -> cons(X,from(s(X)))

The CS-TRS in OBJ format (file Ex6_Luc98.obj):

obj Ex6_Luc98 is
  sort S .
  op first : S S -> S .
  op 0 : -> S .
  op nil : -> S .
  op s : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  vars X Y Z : S .
  eq first(0,X) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
  eq from(X) = cons(X,from(s(X))) .
endo

Negative results

Positive results

1. Ex6_Luc98 can be proved µ-terminating by using Lucas' transformation. The TRS Ex6_Luc98_L:

       first(0,X) -> nil
       first(s(X),cons(Y)) -> cons(Y)
       from(X) -> cons(X)
       

   can be proved terminating (use MuTerm).
2. Ex6_Luc98 can be proved µ-terminating by using Zantema's transformation. The TRS Ex6_Luc98_Z:

       first(0,X) -> nil
       first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
       from(X) -> cons(X,n__from(s(X)))
       first(X1,X2) -> n__first(X1,X2)
       from(X) -> n__from(X)
       activate(n__first(X1,X2)) -> first(X1,X2)
       activate(n__from(X)) -> from(X)
       activate(X) -> X
       

   can be proved terminating (use MuTerm).
3. The µ-termination of Ex6_Luc98 can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex6_Luc98_FR:

      first(0,X) -> nil
      first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
      from(X) -> cons(X,n__from(n__s(X)))
      first(X1,X2) -> n__first(X1,X2)
      from(X) -> n__from(X)
      s(X) -> n__s(X)
      activate(n__first(X1,X2)) -> first(activate(X1),activate(X2))
      activate(n__from(X)) -> from(activate(X))
      activate(n__s(X)) -> s(activate(X))
      activate(X) -> X
      

   can be proved terminating (use CiME).
4. The µ-termination of Ex6_Luc98 can also be proved by using Giesl and Middeldorp's transformation: the TRS Ex6_Luc98_GM:

       a__first(0,X) -> nil
       a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
       a__from(X) -> cons(mark(X),from(s(X)))
       mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
       mark(from(X)) -> a__from(mark(X))
       mark(0) -> 0
       mark(nil) -> nil
       mark(s(X)) -> s(mark(X))
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       a__first(X1,X2) -> first(X1,X2)
       a__from(X) -> from(X)
       

   can be proved terminating (use MuTerm).
5. The µ-termination of Ex6_Luc98 is proved in [BLR02, Example 7] by using CSRPO and also computed automatically by MuTerm:
6. The µ-termination of Ex6_Luc98 can also be proved by using a polynomial interpretation (computed by MuTerm):

       Proof of termination for CS-TRS  Ex6_Luc98:
   
       [first](X1,X2) = X1 + 2.X2
       [0] = 1
       [nil] = 0
       [s](X) = X
       [cons](X1,X2) = X1 + 1
       [from](X) = X + 2
       

7. The µ-termination of Ex6_Luc98 can also be proved by using CSDP(computed by MuTerm).